$\forall$${\it es}$:ES, $i$, $x$, $y$:Id, $I$:(vartype($i$;$x$)$\rightarrow$vartype($i$;$y$)$\rightarrow$Prop).
\\[0ex]$\forall$$e$@$i$. first($e$) $\Rightarrow$ $I$($x$ when $e$,$y$ when $e$)
\\[0ex]\& $\forall$$e$@$i$. $I$($x$ when $e$,$y$ when $e$) $\Rightarrow$ $I$(($x$ after $e$),($y$ after $e$))
\\[0ex]$\Rightarrow$ @$i$ always.$I$($x$,$y$)